refactor(StakeManager): optimize stake, account init and lock function #130

3esmit · 2024-09-23T14:26:06Z

Description

This pull request focuses solely on cleaning up the code. The clean-up removes outdated or unnecessary code, which was masking a bug that is being addressed in #127

Details

This changes the account initialization on stake():

removing zombie instructions, inherited from restaking ability which was removed:
- account was having bonusMP += and totalMP +=, but these values were always zero;
making it more clear, by removing _mintBonusMP, and initializing account on a single write;
allowing the StakeVault to be recycled after unstaking all funds, by removing the check for lockUntil != 0

This changes the method lock():

making it more clear, by removing _mintBonusMP
fixing a bug which was updating lastMint on lock()->_mintBonusMP to current block.timestamp(), which shouldnt be updated to that value, masking the bug addressed in fix(StakeManager): fix finalizeEpoch to use last epoch epochEnd #127

Details on #127 bug

The bug was hidden because the _mintBonusMP function contained a line that updated account.lastMint to the same value as startEpoch. This had the unintended effect of making the epoch estimation appear correct when calling StakeManager.lock(). As a result, the underlying bug wasn’t detected in test_UpdateLockupPeriod.

PR #130 does not fix this bug; instead, it cleans up the code that was hiding it for test_UpdateLockupPeriod to cach it. The actual bug fix is handled in PR #127, which also introduces other tests that would have catched it while implementing the multiplier points estimation.

Purpose

Code Cleanup: This PR removes code that was masking the bug, allowing the system to function properly moving forward.
Not a Bug Fix: It doesn't directly fix the bug but removes the part of the code that was preventing the issue from being caught in the test.

Important Notes

The test failures seen in executeAccount->processAccount->mintMP are unrelated to this cleanup. However, PR #130 requires that PR #127 and PR #129 be merged first to ensure proper function.

Checklist

Ensure you completed all of the steps below before submitting your pull request:

0x-r4bbit · 2024-09-25T14:52:51Z

Changes look good to me, but it seems this is not passing tests

3esmit · 2024-09-25T17:33:11Z

Updated description to explain exactly whats happening here, why this tests are failing for this correct code change.

3esmit · 2024-09-27T02:21:52Z

So this PR is failing on verify because the spec is outdated.

Two things are failing:

The current spec considers restaking is possible (why it didn't failed earlier, btw?)
What is failing is that is havocing inside account, adding some random multiplier points, and see if it incrases (in stake function). However, now the staking contract dont allow restake, and it should not increase anymore.
Here I tested a change in this code where it would add the old balance back again https://prover.certora.com/output/585415/7c5efd9e4bbf4d889c36e9acaada8ee6?anonymousKey=303a179377435cf7b148f082d0a45e0380ddde64
I need @0x-r4bbit some input here on how to update this spec
The other reason I still didn't figured out (just had time to dig into the one above). It's really strange, because it's saying that is possible that stake function to set the account.epoch > than the currentEpoch.
https://prover.certora.com/output/585415/288f4d626b9f412f8f7f78ec6ce440d7?anonymousKey=36b7b0f8ffdb668e596fed82647c213fce66f774
I'll figure this one out tomorrow, and than we see how to update the spec (or fix the contract).
@0x-r4bbit if you see something let me know, but you don't have to look into this one yet because I didn't spent time with it yet.

0x-r4bbit · 2024-10-02T15:05:42Z

@3esmit I added a commit here with these changes:

adds an accountBonusMPIsZeroIfBalanceIsZero invariant (prover run: https://prover.certora.com/output/6199/d6ef43d62ee34413840f6750a6ee64e4?anonymousKey=8f051bae33f9184ab91bc5538afc4d416d2a88ee)
adds that invariant and the accountCurrentMPIsZeroIfBalanceIsZero invariant to the failing sumOfMultiplierPointsIsMultiplierPoints invariant, which then passes (prover run: https://prover.certora.com/output/6199/ecd475b011ad48008f5b0529fb110c46?anonymousKey=122620db726e46da2696bf1b8eb97fdfa7b1ce9d)

This should do the trick

…ving mintBonusMP function

change The rule is failing since we've removed the `lockUntil > 0` check in `stake` and `processAccount` is no longer used in `stake()`. The rule requires `lockUntil > 0` so it will always fail there and can't find a non-reverting cases (which makes the rule pass). The reason it hasn't happened before was because: The rule required account.lockUntil > 0 Stake required lockUntil > 0 || account balance == 0 Also this commit adds an invariant: add invariant that account balance == 0 => accountMP == 0

… current sumOfMultipliers

This invariant failed as the prover started making wrong assumptions about the relationship between anyone's account's `totalMP` and its `balance`, as well as an account's `bonusMP` and its `balance`. This commit fixes it by adding the necessary invariants to proof the property.

3esmit requested a review from 0x-r4bbit September 24, 2024 15:14

3esmit self-assigned this Sep 24, 2024

3esmit force-pushed the remove-mintBonusMP-function branch from 22db53b to 353a4ff Compare September 25, 2024 18:06

0x-r4bbit approved these changes Sep 26, 2024

View reviewed changes

3esmit force-pushed the remove-mintBonusMP-function branch from 353a4ff to 978b4dc Compare September 26, 2024 19:08

3esmit requested a review from 0x-r4bbit September 27, 2024 02:21

3esmit force-pushed the remove-mintBonusMP-function branch from ff243e7 to ad6328d Compare September 27, 2024 13:55

3esmit changed the title ~~refactor(StakeManager): optimize stake and lock functionality by remo…~~ refactor(StakeManager): optimize stake, account init and lock function Sep 27, 2024

0x-r4bbit force-pushed the remove-mintBonusMP-function branch from 28881ec to 41b4362 Compare September 27, 2024 14:54

3esmit added the type: refactor label Oct 1, 2024

3esmit force-pushed the remove-mintBonusMP-function branch from c2a4851 to 254ea0a Compare October 3, 2024 03:24

3esmit and others added 5 commits October 12, 2024 17:35

refactor(StakeManager): optimize stake and lock functionality by remo…

949fc5f

…ving mintBonusMP function

chore(StakeManager.spec): fix spec to don't load totalMP greater than…

11145ba

… current sumOfMultipliers

chore(StakeManager.spec): fix wrong Sload requirement

b0afd21

3esmit force-pushed the remove-mintBonusMP-function branch from 254ea0a to e5d9a45 Compare October 12, 2024 20:39

3esmit merged commit c0bf36d into develop Oct 13, 2024
8 of 9 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

refactor(StakeManager): optimize stake, account init and lock function #130

refactor(StakeManager): optimize stake, account init and lock function #130

3esmit commented Sep 23, 2024 •

edited

Loading

0x-r4bbit commented Sep 25, 2024

3esmit commented Sep 25, 2024

3esmit commented Sep 27, 2024

0x-r4bbit commented Oct 2, 2024

refactor(StakeManager): optimize stake, account init and lock function #130

refactor(StakeManager): optimize stake, account init and lock function #130

Conversation

3esmit commented Sep 23, 2024 • edited Loading

Description

Details

Details on #127 bug

Purpose

Important Notes

Checklist

0x-r4bbit commented Sep 25, 2024

3esmit commented Sep 25, 2024

3esmit commented Sep 27, 2024

0x-r4bbit commented Oct 2, 2024

3esmit commented Sep 23, 2024 •

edited

Loading